\begin{tabbing}
$\forall$$T$:Type, $L$:($T$ List), $R$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow$es\_realizer\{i:l\}).
\\[0ex]l\_all($L$; $T$; $x$.R{-}Feasible\{i:l\}($R$($x$)))
\\[0ex]$\Rightarrow$ l\_all($L$; $T$; $x$.l\_all($L$; $T$; $y$.(R{-}compat\{i:l\}($R$($x$); $R$($y$)) $\vee$ ($x$ = $y$ $\in$ $T$))))
\\[0ex]$\Rightarrow$ R{-}Feasible\=\{i:l\}\+
\\[0ex](Rall($L$; $x$.$R$($x$)))
\-
\end{tabbing}